$\forall$${\it es}$:event\_system\{i:l\}, $e$:es{-}E(${\it es}$), $x$:Id, $T$:Type. \\[0ex]es{-}dtype(${\it es}$; loc($e$); $x$; $T$) \\[0ex]$\Rightarrow$ ($\uparrow$es{-}first(${\it es}$; $e$)) \\[0ex]$\Rightarrow$ (es{-}when(${\it es}$; $x$; $e$) = es{-}initially(${\it es}$; loc($e$); $x$) $\in$ $T$)